[]!P(sys) == (run:Run. (sys(run))) & (run:Run. (sys(run))  (P(run))) 

latex

---

clarification:

box!(Run;P)(sys) == (run:Run. (sys(run))) & (run:Run. (sys(run))  (P(run))) 

latex

Definitions	P & Q, x:A. B(x), x:A. B(x), P  Q
FDL editor aliases	box!